Automated verification of equivalence properties of cryptographic protocols
Identifieur interne : 000126 ( Main/Exploration ); précédent : 000125; suivant : 000127Automated verification of equivalence properties of cryptographic protocols
Auteurs : Rohit Chadha [États-Unis] ; Vincent Cheval [France] ; Tefan Ciobâc [Roumanie, France] ; Steve Kremer [France]Source :
- ACM Transactions on Computational Logic [ 1529-3785 ] ; 2016.
Abstract
Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory isgenerated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.
Url:
Affiliations:
- France, Roumanie, États-Unis
- Franche-Comté, Grand Est, Lorraine (région)
- Besançon, Metz, Nancy
- Université de Bourgogne Franche-Comté, Université de Franche-Comté, Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 001091
- to stream Hal, to step Curation: 001091
- to stream Hal, to step Checkpoint: 000139
- to stream Main, to step Merge: 000171
- to stream Main, to step Curation: 000126
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automated verification of equivalence properties of cryptographic protocols</title><author><name sortKey="Chadha, Rohit" sort="Chadha, Rohit" uniqKey="Chadha R" first="Rohit" last="Chadha">Rohit Chadha</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-48680" status="INCOMING"><orgName>University of Missouri</orgName><desc><address><country key="US"></country></address></desc><listRelation><relation active="#struct-364580" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-364580" type="direct"><org type="institution" xml:id="struct-364580" status="INCOMING"><orgName>UNIVERSITY OF MISSOURI</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>États-Unis</country></affiliation></author><author><name sortKey="Cheval, Vincent" sort="Cheval, Vincent" uniqKey="Cheval V" first="Vincent" last="Cheval">Vincent Cheval</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-445522" status="VALID"><idno type="RNSR">201622052E</idno><orgName>Proof techniques for security protocols</orgName><orgName type="acronym">PESTO</orgName><date type="start">2016-01-01</date><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/pesto</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Ciobac, Tefan" sort="Ciobac, Tefan" uniqKey="Ciobac " first=" Tefan" last="Ciobâc"> Tefan Ciobâc</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-239761" status="VALID"><orgName>CS Department, Al.I. Cuza University, Iasi, Romania</orgName><orgName type="acronym">CS Department, Al.I. Cuza University, Iasi, Romania</orgName><desc><address><addrLine>Iasi</addrLine><country key="RO"></country></address></desc><listRelation><relation active="#struct-242365" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-242365" type="direct"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Roumanie</country><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><country>France</country><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName></affiliation></author><author><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-445522" status="VALID"><idno type="RNSR">201622052E</idno><orgName>Proof techniques for security protocols</orgName><orgName type="acronym">PESTO</orgName><date type="start">2016-01-01</date><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/pesto</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-01306561</idno><idno type="halId">hal-01306561</idno><idno type="halUri">https://hal.inria.fr/hal-01306561</idno><idno type="url">https://hal.inria.fr/hal-01306561</idno><date when="2016">2016</date><idno type="wicri:Area/Hal/Corpus">001091</idno><idno type="wicri:Area/Hal/Curation">001091</idno><idno type="wicri:Area/Hal/Checkpoint">000139</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000139</idno><idno type="wicri:doubleKey">1529-3785:2016:Chadha R:automated:verification:of</idno><idno type="wicri:Area/Main/Merge">000171</idno><idno type="wicri:Area/Main/Curation">000126</idno><idno type="wicri:Area/Main/Exploration">000126</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Automated verification of equivalence properties of cryptographic protocols</title><author><name sortKey="Chadha, Rohit" sort="Chadha, Rohit" uniqKey="Chadha R" first="Rohit" last="Chadha">Rohit Chadha</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-48680" status="INCOMING"><orgName>University of Missouri</orgName><desc><address><country key="US"></country></address></desc><listRelation><relation active="#struct-364580" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-364580" type="direct"><org type="institution" xml:id="struct-364580" status="INCOMING"><orgName>UNIVERSITY OF MISSOURI</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>États-Unis</country></affiliation></author><author><name sortKey="Cheval, Vincent" sort="Cheval, Vincent" uniqKey="Cheval V" first="Vincent" last="Cheval">Vincent Cheval</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-445522" status="VALID"><idno type="RNSR">201622052E</idno><orgName>Proof techniques for security protocols</orgName><orgName type="acronym">PESTO</orgName><date type="start">2016-01-01</date><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/pesto</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Ciobac, Tefan" sort="Ciobac, Tefan" uniqKey="Ciobac " first=" Tefan" last="Ciobâc"> Tefan Ciobâc</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-239761" status="VALID"><orgName>CS Department, Al.I. Cuza University, Iasi, Romania</orgName><orgName type="acronym">CS Department, Al.I. Cuza University, Iasi, Romania</orgName><desc><address><addrLine>Iasi</addrLine><country key="RO"></country></address></desc><listRelation><relation active="#struct-242365" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-242365" type="direct"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Roumanie</country><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><country>France</country><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName></affiliation></author><author><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-445522" status="VALID"><idno type="RNSR">201622052E</idno><orgName>Proof techniques for security protocols</orgName><orgName type="acronym">PESTO</orgName><date type="start">2016-01-01</date><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/pesto</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author></analytic><series><title level="j">ACM Transactions on Computational Logic</title><idno type="ISSN">1529-3785</idno><imprint><date type="datePub">2016</date></imprint></series></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory isgenerated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.</div></front></TEI><affiliations><list><country><li>France</li><li>Roumanie</li><li>États-Unis</li></country><region><li>Franche-Comté</li><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Besançon</li><li>Metz</li><li>Nancy</li></settlement><orgName><li>Université de Bourgogne Franche-Comté</li><li>Université de Franche-Comté</li><li>Université de Lorraine</li></orgName></list><tree><country name="États-Unis"><noRegion><name sortKey="Chadha, Rohit" sort="Chadha, Rohit" uniqKey="Chadha R" first="Rohit" last="Chadha">Rohit Chadha</name></noRegion></country><country name="France"><region name="Grand Est"><name sortKey="Cheval, Vincent" sort="Cheval, Vincent" uniqKey="Cheval V" first="Vincent" last="Cheval">Vincent Cheval</name></region><name sortKey="Kremer, Steve" sort="Kremer, Steve" uniqKey="Kremer S" first="Steve" last="Kremer">Steve Kremer</name></country><country name="Roumanie"><region name="Franche-Comté"><name sortKey="Ciobac, Tefan" sort="Ciobac, Tefan" uniqKey="Ciobac " first=" Tefan" last="Ciobâc"> Tefan Ciobâc</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000126 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000126 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-01306561
|texte= Automated verification of equivalence properties of cryptographic protocols
}}
| This area was generated with Dilib version V0.6.33. |  |